(set-logic ALL)
(set-info :status unsat)
(declare-sort $$unsorted 0)
(declare-sort tptp.student 0)
(declare-sort tptp.professor 0)
(declare-sort tptp.course 0)
(declare-fun tptp.michael () tptp.student)
(declare-fun tptp.victor () tptp.professor)
(declare-fun tptp.csc410 () tptp.course)
(declare-fun tptp.enrolled (tptp.student tptp.course) Bool)
(declare-fun tptp.teaches (tptp.professor tptp.course) Bool)
(declare-fun tptp.taughtby (tptp.student tptp.professor) Bool)
(declare-fun tptp.coordinatorof (tptp.course) tptp.professor)
(assert (forall ((X tptp.student)) (exists ((Y tptp.course)) (tptp.enrolled X Y))))
(assert (forall ((X tptp.professor)) (exists ((Y tptp.course)) (tptp.teaches X Y))))
(assert (forall ((X tptp.course)) (exists ((Y tptp.student)) (tptp.enrolled Y X))))
(assert (forall ((X tptp.course)) (exists ((Y tptp.professor)) (tptp.teaches Y X))))
(assert (forall ((X tptp.course)) (tptp.teaches (tptp.coordinatorof X) X)))
(assert (forall ((X tptp.student) (Y tptp.course)) (=> (tptp.enrolled X Y) (forall ((Z tptp.professor)) (=> (tptp.teaches Z Y) (tptp.taughtby X Z))))))
(assert (tptp.enrolled tptp.michael tptp.csc410))
(assert (= (tptp.coordinatorof tptp.csc410) tptp.victor))
(assert (not (tptp.taughtby tptp.michael tptp.victor)))
(set-info :filename tff0)
(check-sat-assuming ( true ))
